package bcontractor.propositional;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.StringTokenizer;

import org.apache.commons.lang.StringUtils;

import bcontractor.api.SentenceSet;
import bcontractor.base.SetUtils;

public class SentenceParser {

    private static final String NOT = "¬";
    private static final String OR = " v ";
    private static final String AND = "^";

    private int counter = 0;
    private Map<String, Integer> atomMap = new HashMap<String, Integer>();

    public SentenceSet<PropositionalSentence> createSet(String... sentences) {
        return SetUtils.<PropositionalSentence> emptySentenceSet().with(this.createList(sentences));
    }

    public List<PropositionalSentence> createList(String... sentences) {
        List<PropositionalSentence> parsed = new ArrayList<PropositionalSentence>(sentences.length);
        for (String sentence : sentences) {
            parsed.add(this.create(sentence));
        }
        return parsed;
    }

    public PropositionalSentence create(String sentence) {
        int[][] dimacsSentence = new int[StringUtils.countMatches(sentence, AND) + 1][];
        StringTokenizer clauseTokenizer = new StringTokenizer(sentence, AND);
        int clauseIndex = -1;
        while (clauseTokenizer.hasMoreTokens()) {
            String clause = clauseTokenizer.nextToken().replaceAll("\\(|\\)", "").trim();
            int[] dimacsClause = new int[StringUtils.countMatches(clause, OR) + 1];
            StringTokenizer literalTokenizer = new StringTokenizer(clause, OR);
            int literalIndex = -1;
            while (literalTokenizer.hasMoreTokens()) {
                String literal = literalTokenizer.nextToken().trim();
                boolean negative = literal.startsWith(NOT);
                String atom = negative ? literal.substring(1) : literal;
                if (!this.atomMap.containsKey(atom)) {
                    this.atomMap.put(atom, ++this.counter);
                }
                dimacsClause[++literalIndex] = negative ? -this.atomMap.get(atom) : this.atomMap.get(atom);
            }
            dimacsSentence[++clauseIndex] = dimacsClause;
        }
        return new PropositionalSentence(dimacsSentence);
    }
}
